Make documentation build works outside of git repository
Origin: other
Last-Update: 2019-01-03
Current documentation build requires git and curl to get some stuff from the internet
This patch aims to delete those dependencies, forcing git branch to master,
and using Debian provided plantuml instead of downloading it from apache mirror
Last-Update: 2019-01-03
Gbp-Pq: Name 0006-fix-doc-build.patch